from deslab import *

def iscontrollable(H,G):    
    controllable = True
    Sigma_uc = G.Sigma - G.Sigcon
    H0 = product(H,G)   
    for (y,x) in H0.X:
        G_events_uc =  G.Gamma(x) & Sigma_uc
        if not H0.Gamma((y,x)) >= G_events_uc:
            controllable = False  
    return controllable
    
    
def supcontrollable(H,G):
    if ispfclosed(H):
        print 'Using Prefix Closed Algorithm'
        Ksupc = supcontrollablepfclosed(H,G)
    else:
        print 'Using General Algorithm'
        Ksupc =  supcontrollablegeneral(H,G) 
       
    if Ksupc <> fsa():
        Ksupc = Ksupc.renamestates('number')
       
    Ksupc= Ksupc.setpar(name ='$K^{{\uparrow}C}$')
    return Ksupc
   

def supcontrollablegeneral(H,G):
    Sigma_uc = G.Sigma - G.Sigcon
    H0 = H&G.setpar(Xm = G.X)
    H0_changed = True
    while (H0_changed & (H0 <> fsa())):
        H0_changed = False
        for (y,x) in H0.X:
            G_events_uc = G.Gamma(x) & Sigma_uc
            if not(G_events_uc <= H0.Gamma((y,x))):
                H0 = H0.deletestate((y,x))
                H0_changed = True                           
        H0 = trim(H0)   
    return H0
   
   
def supcontrollablepfclosed(H,G):
    E_clos = sigmakleeneclos(G.Sigma)   
    Sigma_uc = G.Sigma - G.Sigcon
    E_uc_clos = sigmakleeneclos(Sigma_uc)
    
    #Ksupc = H-(((G-H)/E_uc_clos)*E_clos)
    Ksupc = H-(langquotient(G-H,E_uc_clos,G2kleenclos=True)*E_clos)
    
    return Ksupc

      
def isobservable(H,G,method=''):  
    if method and (method in 'cassandras'):
        return obstest_cassandras(H,G)
    elif method and (method in 'obstodiag'):
        return obstest_obstodiag(H,G)        
    else:
        return obstest_smart(H,G)
    
def obsverifier(H,G,method=''):  
    if method and (method in 'cassandras'):
        return obsverifier_cassandras(H,G)
    elif method and (method in 'obstodiag'):
        return obsverifier_obstodiag(H,G)
    else:
        return obsverifier_smart(H,G)       
    
def obstest_cassandras(H,G):        
    if trim(obsverifier_cassandras(H,G,stop=True)) <> fsa():
        return False
    else:
        return True 
        
def obsverifier_cassandras(H,G,stop = False):  
        
    def createstateandtrans(X_new,E_new):
        if not(X_new in X):
            X.append(X_new)
            if X_new <> dead:
                X_new_string = '(' + str(X_new[0]) + ',' + str(X_new[1]) + ',' + str(X_new[2]) + ')'
                Table.update({X_new: X_new_string})
            if X_new <> dead:
                S.append(X_new)            
        
        if not(E_new in E):
            E.append(E_new)
        E_new_string = str(E_new[0]) + '.' + str(E_new[1]) + '.' + str(E_new[2])
        Table.update({E_new: E_new_string})
        
        T_new = (state,E_new,X_new)
        if not(T_new in T):
            T.append(T_new) 
            
    Hm = H.setpar(Xm = H.X)
    Gm = G.setpar(Xm = G.X)      

    dead = 'dead'
    eps = 'epsilon'
    
    X0 = (iter(Hm.X0).next(),iter(Hm.X0).next(),iter(Gm.X0).next())
    X = [X0]
    E = []
    T = []
    Table = {X0: '(' + str(X0[0]) + ',' + str(X0[1]) + ',' + str(X0[2]) + ')'}
    
    S = [X0]   
    while S <> []:
        state = S.pop()        
        
        H1_Gamma = Hm.Gamma(state[0])
        H2_Gamma = Hm.Gamma(state[1])
        G_Gamma = Gm.Gamma(state[2])

        active_events = H1_Gamma.union(H2_Gamma)
        
        for event in active_events:
            if event in Gm.Sigobs:
                if (event in H1_Gamma) and (event in H2_Gamma) and (event in G_Gamma):                    
                    X_new = (Hm.delta(state[0],event),Hm.delta(state[1],event),Gm.delta(state[2],event))
                    E_new = (event,event,event)
                    createstateandtrans(X_new,E_new)
                elif (event in Gm.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    X_new = dead
                    E_new = (event,eps,event)
                    createstateandtrans(X_new,E_new)
                    if stop:
                        S = []
                        break
            else:
                if (event in H1_Gamma):
                    X_new = (Hm.delta(state[0],event),state[1],state[2])
                    E_new = (event,eps,eps)
                    createstateandtrans(X_new,E_new)
                if (event in H2_Gamma) and (event in G_Gamma):
                    X_new = (state[0],Hm.delta(state[1],event),Gm.delta(state[2],event))
                    E_new = (eps,event,event)
                    createstateandtrans(X_new,E_new)
                if (event in Gm.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    X_new = dead                    
                    E_new = (event,eps,event)
                    createstateandtrans(X_new,E_new)
                    if stop:
                        S = []
                        break
    if dead in X:
        Xm = [dead]
    else:
        Xm = []

    V = fsa(X,E,T,X0,Xm,table = Table, name='$V$')  
    V.setgraphic('observer')    
    return V

def obstest_smart(H,G):    

    def verifyobscondition(V):
            
        def isrenamedactive(state,event):
            
            def getrenamed(event):
                s = str(event)
                if '_' in event:
                    ind = s.index('_') + 1
                    eventStr = s[:ind] + '{' + s[ind:] + '_R}'
                else:
                    eventStr = s + '_R'
                return eventStr

            if getrenamed(event) in V.Gamma(state):
                return True
            return False
        
        dump = 'D'
        if V <> fsa():
            for state in V.X:
                if dump == state:
                    for edge in V.Graph.in_edges_iter(state,keys=True):
                        if (edge[0] <> dump) and (edge[2] in V.Sigcon):
                            if (edge[2] in V.Sigobs):
                                return False
                            elif (edge[0][0] <> edge[0][1]) and isrenamedactive(edge[0],edge[2]): #definedinH(edge[0][0],edge[2]):
                                return False
        return True
            
    return verifyobscondition(obsverifier_smart(H,G))
        
def obsverifier_smart(H,G):  
    
    def renamenonobsevents(auto):
        for event in (auto.Sigma - auto.Sigobs):
            s = str(event)
            if '_' in s:
                ind = s.index('_') + 1
                eventStr = s[:ind] + '{' + s[ind:] + '_R}'
            else:
                eventStr = s + '_R'                                        
            auto = auto.renamevents({ event : eventStr})
        return auto
    
    def createdumpfrommarked(auto):
        for state in auto.Xm:            
            auto = auto.renamestates({ state : dump})
        return auto
    
    def removenameredundancy(auto):
        for state in auto.X - auto.Xm:            
            auto = auto.renamestates({ state : state[0]})
        return auto
          
    dump = 'D'
    
    Gm = G.setpar(name ='$G$')
    
    Hm = H.setpar(Xm = H.X)
    Hm = Hm.setpar(name ='$H_m$')    
        
    Hr = Hm.copy()
    Hr = Hr.setpar(name ='$H_R$')
    Hr = renamenonobsevents(Hr)
    
    Hc = trim(Gm-Hm)
    Hc = Hc.setpar(name ='$H_C$')
    Hcd = createdumpfrommarked(Hc)
    Hcd = Hcd.setpar(name ='$H_C^D$')
    
    Vobs = Hr//Hcd
    Vobs = Vobs.setpar(name ='$V_{obs}$')
    V = createdumpfrommarked(Vobs)
    V = V.setpar(name ='$V$')
    V.setgraphic('observer')
    
    #draw(Gm,Hm,Hr,Hc,Hcd,Vobs,V)
    
    #draw(Gm,'figurecolor')
    #draw(Hm,'figurecolor')
    #draw(Hr,'figurecolor')
    #draw(Hc,'figurecolor')
    #draw(Hcd,'figurecolor')
    #draw(Vobs,'figurecolor')
    #draw(V,'figurecolor')
            
    return V

def coobstest_smart(H,G):    

    def verifycoobscondition(V):
            
        def isrenamedactive(state,event):
            
            def getrenamed(event):
                s = str(event)
                if '_' in event:
                    ind = s.index('_') + 1
                    eventStr = s[:ind] + '{' + s[ind:] + '_R}'
                else:
                    eventStr = s + '_R'
                return eventStr

            if getrenamed(event) in V.Gamma(state):
                return True
            return False
        
        dump = 'D'
        if V <> fsa():
            for state in V.X:
                if dump == state:
                    for edge in V.Graph.in_edges_iter(state,keys=True):
                        if (edge[0] <> dump) and (edge[2] in V.Sigcon):
                            if (edge[2] in V.Sigobs):
                                return False
                            elif (edge[0][0] <> edge[0][1]) and isrenamedactive(edge[0],edge[2]): #definedinH(edge[0][0],edge[2]):
                                return False
        return True
            
    return verifycoobscondition(coobsverifier_smart(H,G))

def coobsverifier_smart(Hlist,G):  
    
    def renamenonobsevents(auto):
        for event in (auto.Sigma - auto.Sigobs):
            s = str(event)
            if '_' in s:
                ind = s.index('_') + 1
                eventStr = s[:ind] + '{' + s[ind:] + '_R}'
            else:
                eventStr = s + '_R'                                        
            auto = auto.renamevents({ event : eventStr})
        return auto
    
    def createdumpfrommarked(auto):
        for state in auto.Xm:            
            auto = auto.renamestates({ state : dump})
        return auto
    
    dump = 'D'
    
    Gm = G.setpar(name ='$G$')
    
    Hrlist = list()
    Hrtotal = fsa()
    i = 1
    for H in Hlist:
        Hm = H.setpar(Xm = H.X)
        Hm = Hm.setpar(name ='$H_{m,' + str(i) +'}$')
        Hr = Hm.copy()
        Hr = Hr.setpar(name ='$H_{R,' + str(i) +'}$')
        Hr = renamenonobsevents(Hr)
        Hrlist.append(Hr)
        if i > 1:
            Hrtotal = Hrtotal // Hr
        else:
            Hrtotal = Hr            
        i += 1
    
    Hrtotal = Hrtotal.setpar(name ='$H_{R,total}$')
    
    Hc = trim(Gm-Hm)
    Hc = Hc.setpar(name ='$H_C$')
    Hcd = createdumpfrommarked(Hc)
    Hcd = Hcd.setpar(name ='$H_C^D$')
        
    Vobs = Hrtotal//Hcd
    Vobs = Vobs.setpar(name ='$V_{obs}$')
    V = createdumpfrommarked(Vobs)
    #V = Vobs.copy()
    V = V.setpar(name ='$V$')
    V.setgraphic('observer')
    
    draw(Gm,Hrlist[0],Hrlist[1],Hrtotal,Hcd,Vobs,V)
            
    return V
    
def obstest_obstodiag(H,G): 
    from deslab.toolboxes import diagnosis    
     
    Ht, sf = obstodiag(H,G) 
    return diagnosis.is_diagnosable_verif(Ht, sf)[0]
        
def obsverifier_obstodiag(H,G):
    from deslab.toolboxes import diagnosis
    
    Ht, sf = obstodiag(H,G)    
    return diagnosis.is_diagnosable_verif(Ht, sf)[1]
        
def obstodiag(H,G):    
    sf = set()    
    Ht = H.copy()
    
    for event in Ht.Sigcon:
            de = 'd_{' + event + '}'
            ve = 'v_{' + event + '}'
            Ht = Ht.addstate(de)
            Ht = Ht.addtransition([de,ve,de])
            
    for state in H:
        for event in H.Sigcon:
            if event in G.Gamma(state):
                if event in H.Gamma(state):
                    ue = 'u_{' + event + '}'
                    de = 'd_{' + event + '}'
                    sf |= {ue}
                    Ht = Ht.addtransition([state,ue,de])
                else:
                    fe = 'f_{' + event + '}'
                    re = 'r_{' + event + '}'
                    de = 'd_{' + event + '}'                    
                    Ht = Ht.addtransition([state,fe,de])
                    Ht = Ht.addtransition([state,re,de])
                    sf |= {fe}
    z = 'z'
    for state in H:
        if G.Gamma(state) == EMPTYSET:
            Ht = Ht.addtransition([state,z,state])   
            
    Ht = Ht.setpar(Sigobs = Ht.Sigobs - sf)
    Ht = Ht.setpar(Sigcon = H.Sigcon)
    Ht = Ht.setpar(name ='$\\tilde{H}$')
    
    #draw(Ht)
    
    return Ht, sf

def isnormal(H,G):    
    return normalitytest(H,G)


def normalitytest(H,G):    

    def verifynormalitycondition(V):
        if V.Xm <> EMPTYSET:
            return False
        return True
            
    return verifynormalitycondition(normalityverifier(H,G))

def normalityverifier(H,G):
    return(obsverifier_smart(H,G))
    

def supnormal(H,G):
    if ispfclosed(H):
        print 'Using Prefix Closed Algorithm'
        Ksupn = supnormalpfclosed(H,G)
    else:
        print 'Using General Algorithm'
        Ksupn =  supnormalgeneral(H,G) 
       
    if Ksupn <> fsa():
        Ksupn = Ksupn.renamestates('number')
       
    Ksupn = Ksupn.setpar(name ='$K^{{\uparrow}N}$')
    return Ksupn   

def supnormalgeneral(H,G):
    Knext = H.copy()
    Knextm = H.copy()
    Ksupn = fsa()
    
    while not are_langequiv(Knextm,Ksupn):
        Kpc = Knext.setpar(Xm = Knext.X)
        Ksupn = supnormalpfclosed(Kpc,G)
        Knext = Ksupn - complement(H)
        Knextm = Knext.setpar(Xm = Knext.X)
        
    return Knext
   
def supnormalpfclosed(H,G):
    E_clos = sigmakleeneclos(G.Sigma)  
    
    #Ksupn = H-((invproj(proj(G-H,G.Sigobs),G.Sigma))*E_clos)
    P = proj(G-H)
    I = invobsproj(P,G.Sigma)
    EX = I*E_clos
    Ksupn = H-EX    
        
    return Ksupn

def supcontrollablenormal(H,G):    
    Ksupcn = H.copy()
    Kprev = fsa()
    
    while not are_langequiv(Ksupcn,Kprev):
        Kprev = Ksupcn
        Ksupc = supcontrollable(Ksupcn,G)
        Ksupcn = supnormal(Ksupc,G)
        
    if Ksupcn <> fsa():
        Ksupcn = Ksupcn.renamestates('number')       
    Ksupcn = Ksupcn.setpar(name ='$K^{{\uparrow}(CN)}$')
       
    return Ksupcn